IsIntegDom(r) == 0  1  |r|  & (u, v:|r|. ((v = 0))  ((u * v) = 0)  (u = 0)) 

latex

---

clarification:

IsIntegDom(r)
== 0r  1r  |r| 
== & (u:|r|, v:|r|. ((v = (0r)  |r|))  ((u (*r) v) = (0r)  |r|)  (u = (0r)  |r|)) 

latex

Up	rings 1
Wellformedness Lemmas	integ dom p wf
Definitions	P & Q, a  b  T , 1, x:A. B(x), A, P  Q, x f y, *, |r|, 0